package at.fhj.ase;

public class Square {
	
	
	private static final boolean exceptionDefect1 = false;
	private static final boolean exceptionDefect2 = false;
	
	/**
	 * @param x value for which square root is desired
	 * @return calculated square root value
	 */
	/*@
	  @ public                          // (1)
	  @        normal_behavior          // (2)
	  @ requires x >= 0;                // (3)
	  @ ensures \result * \result <= x; // (4)
	  @ ensures x < (Math.abs(\result) + 1) *
	  @             (Math.abs(\result) + 1);
	  @ assignable \nothing;            // (5)
	  @ also
	  @ public exceptional_behavior
	  @ requires x < 0;
	  @ signals_only IllegalArgumentException;
	  @ assignable \nothing;
	  @*/
	public static int iSqrt (int x) {
		
		double dResult =  0.0;
		boolean throwNeg = x < 0;
		if (exceptionDefect1) {
			throwNeg = true;
		} else if (exceptionDefect2) {
			throwNeg = false;
		}

		if (throwNeg) {
			throw new IllegalArgumentException("Arg negative = "+x);
		}
		dResult =  Math.sqrt((double) x);
//		System.out.println("dResult ("+x+") = "+dResult);
		return (int) dResult;
	}

	/**
	 * @param args not used
	 */
	public static void main(String[] args) {
		for (int i = 1; i <= 20; i++) {
			doTestCase(i);
		}
		doTestCase(-1);
		doTestCase(-10);
//		doTestCase(Integer.MAX_VALUE);
	}
	
	private static void doTestCase (int x) {
		try {
			System.out.print ("iSqrt("+x+") = ");
			System.out.flush();
			int sqrtVal = iSqrt(x);
			System.out.println (sqrtVal);
		} catch (IllegalArgumentException e) {
			System.out.println ("Caught exception: "+e.getMessage());
		}
		
	}
	

}
